package tr.edu.ege.kipler.satisfiability;

import java.util.LinkedHashSet;
import java.util.Set;
import java.util.Stack;

import tr.edu.ege.kipler.satisfiability.completion.CompletionStrategy;
import tr.edu.ege.kipler.satisfiability.completion.rules.RuleLogger;
import tr.edu.ege.kipler.satisfiability.completion.rules.nondeterminism.BranchingPoint;
import tr.edu.ege.kipler.satisfiability.completion.rules.nondeterminism.LinearBranchingPoint;
import tr.edu.ege.kipler.satisfiability.container.WorldConstraintSystem;
import tr.edu.ege.kipler.satisfiability.container.operational.IndividualNameManager;
import tr.edu.ege.kipler.satisfiability.profile.ReasoningProfile;
import tr.edu.ege.kipler.syntax.WorldElement;

/**
 * This is the default implementation of the {@link Reasoner} interface.
 * 
 * @author İnanç Seylan
 * 
 */
public class GenericReasoner implements Reasoner {

	private WorldConstraintSystem currentWcs;

	private BranchingPoint currentPoint;

	/**
	 * This stack is used to simulate the tree characteristic of the tableau
	 * algorithm. Each application of a branching rule generates a new world
	 * constraint system. We have to consider each of these world constraint
	 * systems until one is found that is complete and satisfiable. This stack
	 * allows us to visit these world constraint systems as if we're traversing
	 * a tree.
	 */
	private Stack<BranchingPoint> branchingStack = new Stack<BranchingPoint>();

	private int lastWcsId;

	private ReasoningProfile profile;

	private Set<WorldElement> formulaSet = new LinkedHashSet<WorldElement>();

	public GenericReasoner() {
	}

	public ReasoningProfile getProfile() {
		return profile;
	}

	public void setProfile(ReasoningProfile profile) {
		this.profile = profile;
	}

	/**
	 * This method should only be called after {@link #isSatisfiable()} or
	 * {@link #isLogicalConsequence(WorldElement)}.
	 * 
	 * @return the last {@link WorldConstraintSystem} that the reasoner had
	 *         modified when the tableau algorithm ended.
	 */
	public WorldConstraintSystem getCurrentWcs() {
		return currentWcs;
	}

	/**
	 * @see Reasoner#addFormula(WorldElement)
	 */
	public void addFormula(WorldElement formula) {
		formulaSet.add(formula);
	}

	/**
	 * @see Reasoner#addFormulas(Set)
	 */
	public void addFormulas(Set<WorldElement> formulas) {
		formulaSet.addAll(formulas);
	}

	/**
	 * Applies the rules of tableau to all worlds in a world constraint system.
	 * The case of the disjunction rule is treated specially. If the disjunction
	 * rule is applied to a wcs, this method ends for that wcs.
	 * 
	 */
	private void applyRules() throws ReasonerException {
		CompletionStrategy cs = getProfile().getCompletionStrategy();
		if (cs != null) {
			cs.apply(getCurrentWcs());
		}
	}

	/**
	 * Adds the branching point to the stack.
	 */
	public void addBranch(BranchingPoint bp) {
		branchingStack.push(bp);
	}

	private WorldConstraintSystem preprocess(Set<WorldElement> formulaSet) {
		return getProfile().getPreprocessingStrategy().process(formulaSet);
	}

	/**
	 * @see Reasoner#isSatisfiable()
	 */
	public boolean isSatisfiable() throws Exception {
		return isSatisfiable(formulaSet);
	}

	/**
	 * This method actually applies the satisfiability checking algorithm on the
	 * knowledge base plus the negation of the input formula.
	 * 
	 * @return true if the knowledge base plus the negation of the input formula
	 *         is unsatisfiable.
	 * @see Reasoner#isLogicalConsequence(WorldElement)
	 */
	public boolean isLogicalConsequence(WorldElement formula) throws Exception {
		WorldElement negFormula = formula.copy().toggleNegated();
		Set<WorldElement> formulaSetCopy = new LinkedHashSet<WorldElement>(
				formulaSet);
		formulaSetCopy.add(negFormula);
		return !isSatisfiable(formulaSetCopy);
	}

	private void initProver(WorldConstraintSystem wcs) {
		lastWcsId = 0;
		IndividualNameManager.getInstance().reset();
		currentWcs = wcs;
		currentWcs.setId(lastWcsId);
		currentWcs.getData().getLogger().setEnabled(
				getProfile().isLoggingEnabled());
		branchingStack.clear();
	}

	private boolean isSatisfiable(Set<WorldElement> formulaSet) {
		WorldConstraintSystem initialWcs = preprocess(formulaSet);
		initProver(initialWcs);
		// if the initial world constraint system is unsatisfiable already
		if (!initialWcs.getWorld("w0").isSatisfiable()) {
			return false;
		}
		boolean satisfiable = false;
		currentPoint = new LinearBranchingPoint(currentWcs);
		do {
			try {
				currentWcs = currentPoint.next();
				applyRules();
				satisfiable = true;
			} catch (BranchingException e) {
				satisfiable = false;
				// next iteration for depth-first traversal
				currentPoint = branchingStack.peek();
			} catch (UnsatisfiableException e) {
				satisfiable = false;
				getLogger().info(
						"WCS " + getCurrentWcs().getId()
								+ " is unsatisfiable. Cause "
								+ e.getExplanation());
				if (getProfile().isBackjumpingEnabled()) {
					backjump(e.getDependencySet());
				} else {
					backtrack();
				}
			} catch (ReasonerException e) {
				// will never come here
			}
		} while (currentPoint.hasNext() && !satisfiable);
		return satisfiable;
	}

	private RuleLogger getLogger() {
		return currentWcs.getData().getLogger();
	}

	/**
	 * 
	 */
	private void backtrack() {
		while (!currentPoint.hasNext() && branchingStack.size() > 1) {
			branchingStack.pop();
			currentPoint = branchingStack.peek();
		}
		currentPoint.getWcs().getData().getLogger().info(
				"Backtracked to WCS " + currentPoint.getWcs().getId());
	}

	private void backjump(Set<WorldConstraintSystem> dependencySet) {
		while (!dependencySet.contains(currentPoint.getWcs())
				&& branchingStack.size() > 1) {
			branchingStack.pop();
			currentPoint = branchingStack.peek();
		}
		// we couldn't find the source of clash; it means the initial wcs is
		// unsatisfiable
		if (!dependencySet.contains(currentPoint.getWcs())) {
			currentPoint = new LinearBranchingPoint(null);
		} else {
			getLogger().info(
					"Backjumped to WCS " + currentPoint.getWcs().getId());
			currentPoint.setLastBranchDependencies(dependencySet);
		}
	}
}
